

LEMMA

If x partially overlaps y and y is disconnected from z, then x is not part of z.
=============================
Step 1

? (all x (all y (all z (((po x y) & (dc y z)) => (~ (p x z))))))


> revsk
=============================
Step 2

? (((~ (po c729239 c729238)) v (~ (dc c729238 c729237))) v (~ (p c729239 c729237)))


> hypdisj
=============================
Step 3

? (~ (p c729239 c729237))

1. (dc c729238 c729237)
2. (po c729239 c729238)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var49 c729239)
|
|1. (p c729239 c729237)
|2. (dc c729238 c729237)
|3. (po c729239 c729238)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p (f724203 c729239 Var56) c729239)
||
||1. (~ (c Var49 c729239))
||2. (p c729239 c729237)
||3. (dc c729238 c729237)
||4. (po c729239 c729238)
||
||> ((p (f724203 X Y) X) <-- (o X Y))
||=============================
||Step 6
||
||? (o c729239 Var56)
||
||1. (~ (p (f724203 c729239 Var56) c729239))
||2. (~ (c Var49 c729239))
||3. (p c729239 c729237)
||4. (dc c729238 c729237)
||5. (po c729239 c729238)
||
||> ((o X Y) <-- (po X Y))
||=============================
||Step 7
||
||? (po c729239 Var56)
||
||1. (~ (o c729239 Var56))
||2. (~ (p (f724203 c729239 Var56) c729239))
||3. (~ (c Var49 c729239))
||4. (p c729239 c729237)
||5. (dc c729238 c729237)
||6. (po c729239 c729238)
||
||> hyp
|=============================
|Step 8
|
|? (c (f724203 c729239 c729238) (f724203 c729239 c729238))
|
|1. (~ (c (f724203 c729239 c729238) c729239))
|2. (p c729239 c729237)
|3. (dc c729238 c729237)
|4. (po c729239 c729238)
|
|> ((c X X) <--)
=============================
Step 9

? (~ (c (f724203 c729239 c729238) c729237))

1. (p c729239 c729237)
2. (dc c729238 c729237)
3. (po c729239 c729238)

> ((~ (c Y X)) <-- (~ (c X Y)))
=============================
Step 10

? (~ (c c729237 (f724203 c729239 c729238)))

1. (c (f724203 c729239 c729238) c729237)
2. (p c729239 c729237)
3. (dc c729238 c729237)
4. (po c729239 c729238)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 11
|
|? (p (f724203 c729239 c729238) c729238)
|
|1. (c c729237 (f724203 c729239 c729238))
|2. (c (f724203 c729239 c729238) c729237)
|3. (p c729239 c729237)
|4. (dc c729238 c729237)
|5. (po c729239 c729238)
|
|> ((p (f724203 X Y) Y) <-- (o X Y))
|=============================
|Step 12
|
|? (o c729239 c729238)
|
|1. (~ (p (f724203 c729239 c729238) c729238))
|2. (c c729237 (f724203 c729239 c729238))
|3. (c (f724203 c729239 c729238) c729237)
|4. (p c729239 c729237)
|5. (dc c729238 c729237)
|6. (po c729239 c729238)
|
|> ((o X Y) <-- (po X Y))
|=============================
|Step 13
|
|? (po c729239 c729238)
|
|1. (~ (o c729239 c729238))
|2. (~ (p (f724203 c729239 c729238) c729238))
|3. (c c729237 (f724203 c729239 c729238))
|4. (c (f724203 c729239 c729238) c729237)
|5. (p c729239 c729237)
|6. (dc c729238 c729237)
|7. (po c729239 c729238)
|
|> hyp
=============================
Step 14

? (~ (c c729237 c729238))

1. (c c729237 (f724203 c729239 c729238))
2. (c (f724203 c729239 c729238) c729237)
3. (p c729239 c729237)
4. (dc c729238 c729237)
5. (po c729239 c729238)

> ((~ (c Y X)) <-- (~ (c X Y)))
=============================
Step 15

? (~ (c c729238 c729237))

1. (c c729237 c729238)
2. (c c729237 (f724203 c729239 c729238))
3. (c (f724203 c729239 c729238) c729237)
4. (p c729239 c729237)
5. (dc c729238 c729237)
6. (po c729239 c729238)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 16

? (dc c729238 c729237)

1. (c c729238 c729237)
2. (c c729237 c729238)
3. (c c729237 (f724203 c729239 c729238))
4. (c (f724203 c729239 c729238) c729237)
5. (p c729239 c729237)
6. (dc c729238 c729237)
7. (po c729239 c729238)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c734468 c734467)) v (o c734468 c734467))


> hypdisj
=============================
Step 3

? (o c734468 c734467)

1. (po c734468 c734467)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c734468 c734467)

1. (~ (o c734468 c734467))
2. (po c734468 c734467)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c739753 c739752)) v (c c739753 c739752))


> hypdisj
=============================
Step 3

? (c c739753 c739752)

1. (o c739753 c739752)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c739752)
|
|1. (~ (c c739753 c739752))
|2. (o c739753 c739752)
|
|> ((p Z X) <-- (~ (c (f734500 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f734500 Var48 c739752 Var51) Var48))
|
|1. (~ (p Var48 c739752))
|2. (~ (c c739753 c739752))
|3. (o c739753 c739752)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f734517 Var57 Var54) Var54)
||
||1. (c (f734500 (f734517 Var57 Var54) c739752 Var51) (f734517 Var57 Var54))
||2. (~ (p (f734517 Var57 Var54) c739752))
||3. (~ (c c739753 c739752))
||4. (o c739753 c739752)
||
||> ((p (f734517 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f734517 Var57 Var54) Var54))
||2. (c (f734500 (f734517 Var57 Var54) c739752 Var51) (f734517 Var57 Var54))
||3. (~ (p (f734517 Var57 Var54) c739752))
||4. (~ (c c739753 c739752))
||5. (o c739753 c739752)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f734500 (f734517 c739753 c739752) c739752 Var51) c739752))
|
|1. (c (f734500 (f734517 c739753 c739752) c739752 Var51) (f734517 c739753 c739752))
|2. (~ (p (f734517 c739753 c739752) c739752))
|3. (~ (c c739753 c739752))
|4. (o c739753 c739752)
|
|> ((~ (c (f734500 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f734517 c739753 c739752) c739752))
|
|1. (c (f734500 (f734517 c739753 c739752) c739752 Var51) c739752)
|2. (c (f734500 (f734517 c739753 c739752) c739752 Var51) (f734517 c739753 c739752))
|3. (~ (p (f734517 c739753 c739752) c739752))
|4. (~ (c c739753 c739752))
|5. (o c739753 c739752)
|
|> hyp
=============================
Step 10

? (c c739753 (f734517 c739753 c739752))

1. (~ (c c739753 c739752))
2. (o c739753 c739752)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f734517 c739753 c739752) c739753)

1. (~ (c c739753 (f734517 c739753 c739752)))
2. (~ (c c739753 c739752))
3. (o c739753 c739752)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f734517 c739753 Var71) c739753)
|
|1. (~ (c (f734517 c739753 c739752) c739753))
|2. (~ (c c739753 (f734517 c739753 c739752)))
|3. (~ (c c739753 c739752))
|4. (o c739753 c739752)
|
|> ((p (f734517 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c739753 Var71)
|
|1. (~ (p (f734517 c739753 Var71) c739753))
|2. (~ (c (f734517 c739753 c739752) c739753))
|3. (~ (c c739753 (f734517 c739753 c739752)))
|4. (~ (c c739753 c739752))
|5. (o c739753 c739752)
|
|> hyp
=============================
Step 14

? (c (f734517 c739753 c739752) (f734517 c739753 c739752))

1. (~ (c (f734517 c739753 c739752) c739753))
2. (~ (c c739753 (f734517 c739753 c739752)))
3. (~ (c c739753 c739752))
4. (o c739753 c739752)

> ((c X X) <--)


LEMMA

Disconnection excludes connection.
=============================
Step 1

? (all x (all y ((dc x y) => (~ (c x y)))))


> revsk
=============================
Step 2

? ((~ (dc c745094 c745093)) v (~ (c c745094 c745093)))


> hypdisj
=============================
Step 3

? (~ (c c745094 c745093))

1. (dc c745094 c745093)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 4

? (dc c745094 c745093)

1. (c c745094 c745093)
2. (dc c745094 c745093)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c750493 c750492)) v (~ (c c750491 c750493))) v (c c750491 c750492))


> hypdisj
=============================
Step 3

? (c c750491 c750492)

1. (c c750491 c750493)
2. (p c750493 c750492)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c750492)
|
|1. (~ (c c750491 c750492))
|2. (c c750491 c750493)
|3. (p c750493 c750492)
|
|> hyp
=============================
Step 5

? (c c750491 c750493)

1. (~ (c c750491 c750492))
2. (c c750491 c750493)
3. (p c750493 c750492)

> hyp


LEMMA

Split x,z into disconnection or connection.
=============================
Step 1

? (all x (all y (all z (((po x y) & (dc y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (po c756048 c756047)) v (~ (dc c756047 c756046))) v ((dc c756048 c756046) v (c c756048 c756046)))


> hypdisj
=============================
Step 3

? (c c756048 c756046)

1. (~ (dc c756048 c756046))
2. (dc c756047 c756046)
3. (po c756048 c756047)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c756048 c756046))

1. (~ (c c756048 c756046))
2. (~ (dc c756048 c756046))
3. (dc c756047 c756046)
4. (po c756048 c756047)

> hyp


LEMMA

In the connected case, x,z are ec or po or z is part of x.
=============================
Step 1

? (all x (all y (all z ((((po x y) & (dc y z)) & (c x z)) => (((ec x z) v (po x z)) v (p z x))))))


> revsk
=============================
Step 2

? ((((~ (po c761869 c761868)) v (~ (dc c761868 c761867))) v (~ (c c761869 c761867))) v (((ec c761869 c761867) v (po c761869 c761867)) v (p c761867 c761869)))


> hypdisj
=============================
Step 3

? (p c761867 c761869)

1. (~ (po c761869 c761867))
2. (~ (ec c761869 c761867))
3. (c c761869 c761867)
4. (dc c761868 c761867)
5. (po c761869 c761868)

> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||=============================
||Step 4
||
||? (o c761869 c761867)
||
||1. (~ (p c761867 c761869))
||2. (~ (po c761869 c761867))
||3. (~ (ec c761869 c761867))
||4. (c c761869 c761867)
||5. (dc c761868 c761867)
||6. (po c761869 c761868)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 5
|||
|||? (c c761869 c761867)
|||
|||1. (~ (o c761869 c761867))
|||2. (~ (p c761867 c761869))
|||3. (~ (po c761869 c761867))
|||4. (~ (ec c761869 c761867))
|||5. (c c761869 c761867)
|||6. (dc c761868 c761867)
|||7. (po c761869 c761868)
|||
|||> hyp
||=============================
||Step 6
||
||? (~ (ec c761869 c761867))
||
||1. (~ (o c761869 c761867))
||2. (~ (p c761867 c761869))
||3. (~ (po c761869 c761867))
||4. (~ (ec c761869 c761867))
||5. (c c761869 c761867)
||6. (dc c761868 c761867)
||7. (po c761869 c761868)
||
||> hyp
|=============================
|Step 7
|
|? (~ (p c761869 c761867))
|
|1. (~ (p c761867 c761869))
|2. (~ (po c761869 c761867))
|3. (~ (ec c761869 c761867))
|4. (c c761869 c761867)
|5. (dc c761868 c761867)
|6. (po c761869 c761868)
|
|> ((~ (p X Z)) <-- (po X Y) (dc Y Z))
||=============================
||Step 8
||
||? (po c761869 Var37)
||
||1. (p c761869 c761867)
||2. (~ (p c761867 c761869))
||3. (~ (po c761869 c761867))
||4. (~ (ec c761869 c761867))
||5. (c c761869 c761867)
||6. (dc c761868 c761867)
||7. (po c761869 c761868)
||
||> hyp
|=============================
|Step 9
|
|? (dc c761868 c761867)
|
|1. (p c761869 c761867)
|2. (~ (p c761867 c761869))
|3. (~ (po c761869 c761867))
|4. (~ (ec c761869 c761867))
|5. (c c761869 c761867)
|6. (dc c761868 c761867)
|7. (po c761869 c761868)
|
|> hyp
=============================
Step 10

? (~ (po c761869 c761867))

1. (~ (p c761867 c761869))
2. (~ (po c761869 c761867))
3. (~ (ec c761869 c761867))
4. (c c761869 c761867)
5. (dc c761868 c761867)
6. (po c761869 c761868)

> hyp


LEMMA

Converse parthood plus failure of forward parthood gives inverse proper part.
=============================
Step 1

? (all x (all y (((p y x) & (~ (p x y))) => (pp-1 x y))))


> revsk
=============================
Step 2

? (((~ (p c768299 c768300)) v (p c768300 c768299)) v (pp-1 c768300 c768299))


> hypdisj
=============================
Step 3

? (pp-1 c768300 c768299)

1. (~ (p c768300 c768299))
2. (p c768299 c768300)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c768299 c768300)

1. (~ (pp-1 c768300 c768299))
2. (~ (p c768300 c768299))
3. (p c768299 c768300)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 5
|
|? (p c768299 c768300)
|
|1. (~ (pp c768299 c768300))
|2. (~ (pp-1 c768300 c768299))
|3. (~ (p c768300 c768299))
|4. (p c768299 c768300)
|
|> hyp
=============================
Step 6

? (~ (p c768300 c768299))

1. (~ (pp c768299 c768300))
2. (~ (pp-1 c768300 c768299))
3. (~ (p c768300 c768299))
4. (p c768299 c768300)

> hyp


LEMMA

Inverse proper part splits into tangential or non-tangential inverse proper part.
=============================
Step 1

? (all x (all y ((pp-1 x y) => ((tpp-1 x y) v (ntpp-1 x y)))))


> revsk
=============================
Step 2

? ((~ (pp-1 c774882 c774881)) v ((tpp-1 c774882 c774881) v (ntpp-1 c774882 c774881)))


> hypdisj
=============================
Step 3

? (ntpp-1 c774882 c774881)

1. (~ (tpp-1 c774882 c774881))
2. (pp-1 c774882 c774881)

> ((ntpp-1 Y X) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c774881 c774882)

1. (~ (ntpp-1 c774882 c774881))
2. (~ (tpp-1 c774882 c774881))
3. (pp-1 c774882 c774881)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f768411 Z X Y) Z)))
|=============================
|Step 5
|
|? (pp c774881 c774882)
|
|1. (~ (ntpp c774881 c774882))
|2. (~ (ntpp-1 c774882 c774881))
|3. (~ (tpp-1 c774882 c774881))
|4. (pp-1 c774882 c774881)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 6
|
|? (pp-1 c774882 c774881)
|
|1. (~ (pp c774881 c774882))
|2. (~ (ntpp c774881 c774882))
|3. (~ (ntpp-1 c774882 c774881))
|4. (~ (tpp-1 c774882 c774881))
|5. (pp-1 c774882 c774881)
|
|> hyp
=============================
Step 7

? (~ (ec (f768411 c774881 c774882 Var44) c774881))

1. (~ (ntpp c774881 c774882))
2. (~ (ntpp-1 c774882 c774881))
3. (~ (tpp-1 c774882 c774881))
4. (pp-1 c774882 c774881)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 8
||
||? (pp c774881 Var50)
||
||1. (ec (f768411 c774881 c774882 Var44) c774881)
||2. (~ (ntpp c774881 c774882))
||3. (~ (ntpp-1 c774882 c774881))
||4. (~ (tpp-1 c774882 c774881))
||5. (pp-1 c774882 c774881)
||
||> ((pp Y X) <-- (pp-1 X Y))
||=============================
||Step 9
||
||? (pp-1 Var50 c774881)
||
||1. (~ (pp c774881 Var50))
||2. (ec (f768411 c774881 c774882 Var44) c774881)
||3. (~ (ntpp c774881 c774882))
||4. (~ (ntpp-1 c774882 c774881))
||5. (~ (tpp-1 c774882 c774881))
||6. (pp-1 c774882 c774881)
||
||> hyp
|=============================
|Step 10
|
|? (ec (f768411 c774881 c774882 Var44) c774882)
|
|1. (ec (f768411 c774881 c774882 Var44) c774881)
|2. (~ (ntpp c774881 c774882))
|3. (~ (ntpp-1 c774882 c774881))
|4. (~ (tpp-1 c774882 c774881))
|5. (pp-1 c774882 c774881)
|
|> ((ec (f768411 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 11
||
||? (~ (ntpp c774881 c774882))
||
||1. (~ (ec (f768411 c774881 c774882 Var44) c774882))
||2. (ec (f768411 c774881 c774882 Var44) c774881)
||3. (~ (ntpp c774881 c774882))
||4. (~ (ntpp-1 c774882 c774881))
||5. (~ (tpp-1 c774882 c774881))
||6. (pp-1 c774882 c774881)
||
||> hyp
|=============================
|Step 12
|
|? (pp c774881 c774882)
|
|1. (~ (ec (f768411 c774881 c774882 Var44) c774882))
|2. (ec (f768411 c774881 c774882 Var44) c774881)
|3. (~ (ntpp c774881 c774882))
|4. (~ (ntpp-1 c774882 c774881))
|5. (~ (tpp-1 c774882 c774881))
|6. (pp-1 c774882 c774881)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 13
|
|? (pp-1 c774882 c774881)
|
|1. (~ (pp c774881 c774882))
|2. (~ (ec (f768411 c774881 c774882 Var44) c774882))
|3. (ec (f768411 c774881 c774882 Var44) c774881)
|4. (~ (ntpp c774881 c774882))
|5. (~ (ntpp-1 c774882 c774881))
|6. (~ (tpp-1 c774882 c774881))
|7. (pp-1 c774882 c774881)
|
|> hyp
=============================
Step 14

? (~ (tpp c774881 c774882))

1. (ec (f768411 c774881 c774882 Var44) c774881)
2. (~ (ntpp c774881 c774882))
3. (~ (ntpp-1 c774882 c774881))
4. (~ (tpp-1 c774882 c774881))
5. (pp-1 c774882 c774881)

> ((~ (tpp Y X)) <-- (~ (tpp-1 X Y)))
=============================
Step 15

? (~ (tpp-1 c774882 c774881))

1. (tpp c774881 c774882)
2. (ec (f768411 c774881 c774882 Var44) c774881)
3. (~ (ntpp c774881 c774882))
4. (~ (ntpp-1 c774882 c774881))
5. (~ (tpp-1 c774882 c774881))
6. (pp-1 c774882 c774881)

> hyp


LEMMA

Split into dc(x,z) or c(x,z). In the connected case use Lemma7. If p(z,x), combine with Lemma1 to get pp-1(x,z), then Lemma9 gives tpp-1(x,z) or ntpp-1(x,z).
=============================
Step 1

? (all x (all y (all z (((po x y) & (dc y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp-1 x z)) v (ntpp-1 x z))))))


> revsk
=============================
Step 2

? (((~ (po c781617 c781616)) v (~ (dc c781616 c781615))) v (((((dc c781617 c781615) v (ec c781617 c781615)) v (po c781617 c781615)) v (tpp-1 c781617 c781615)) v (ntpp-1 c781617 c781615)))


> hypdisj
=============================
Step 3

? (ntpp-1 c781617 c781615)

1. (~ (tpp-1 c781617 c781615))
2. (~ (po c781617 c781615))
3. (~ (ec c781617 c781615))
4. (~ (dc c781617 c781615))
5. (dc c781616 c781615)
6. (po c781617 c781616)

> ((ntpp-1 X Y) <-- (pp-1 X Y) (~ (tpp-1 X Y)))
|=============================
|Step 4
|
|? (pp-1 c781617 c781615)
|
|1. (~ (ntpp-1 c781617 c781615))
|2. (~ (tpp-1 c781617 c781615))
|3. (~ (po c781617 c781615))
|4. (~ (ec c781617 c781615))
|5. (~ (dc c781617 c781615))
|6. (dc c781616 c781615)
|7. (po c781617 c781616)
|
|> ((pp-1 X Y) <-- (p Y X) (~ (p X Y)))
||=============================
||Step 5
||
||? (p c781615 c781617)
||
||1. (~ (pp-1 c781617 c781615))
||2. (~ (ntpp-1 c781617 c781615))
||3. (~ (tpp-1 c781617 c781615))
||4. (~ (po c781617 c781615))
||5. (~ (ec c781617 c781615))
||6. (~ (dc c781617 c781615))
||7. (dc c781616 c781615)
||8. (po c781617 c781616)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c781617 c781615)
||||
||||1. (~ (p c781615 c781617))
||||2. (~ (pp-1 c781617 c781615))
||||3. (~ (ntpp-1 c781617 c781615))
||||4. (~ (tpp-1 c781617 c781615))
||||5. (~ (po c781617 c781615))
||||6. (~ (ec c781617 c781615))
||||7. (~ (dc c781617 c781615))
||||8. (dc c781616 c781615)
||||9. (po c781617 c781616)
||||
||||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||||=============================
|||||Step 7
|||||
|||||? (c c781617 c781615)
|||||
|||||1. (~ (o c781617 c781615))
|||||2. (~ (p c781615 c781617))
|||||3. (~ (pp-1 c781617 c781615))
|||||4. (~ (ntpp-1 c781617 c781615))
|||||5. (~ (tpp-1 c781617 c781615))
|||||6. (~ (po c781617 c781615))
|||||7. (~ (ec c781617 c781615))
|||||8. (~ (dc c781617 c781615))
|||||9. (dc c781616 c781615)
|||||10. (po c781617 c781616)
|||||
|||||> ((c X Y) <-- (~ (dc X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (~ (dc c781617 c781615))
|||||
|||||1. (~ (c c781617 c781615))
|||||2. (~ (o c781617 c781615))
|||||3. (~ (p c781615 c781617))
|||||4. (~ (pp-1 c781617 c781615))
|||||5. (~ (ntpp-1 c781617 c781615))
|||||6. (~ (tpp-1 c781617 c781615))
|||||7. (~ (po c781617 c781615))
|||||8. (~ (ec c781617 c781615))
|||||9. (~ (dc c781617 c781615))
|||||10. (dc c781616 c781615)
|||||11. (po c781617 c781616)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (ec c781617 c781615))
||||
||||1. (~ (o c781617 c781615))
||||2. (~ (p c781615 c781617))
||||3. (~ (pp-1 c781617 c781615))
||||4. (~ (ntpp-1 c781617 c781615))
||||5. (~ (tpp-1 c781617 c781615))
||||6. (~ (po c781617 c781615))
||||7. (~ (ec c781617 c781615))
||||8. (~ (dc c781617 c781615))
||||9. (dc c781616 c781615)
||||10. (po c781617 c781616)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (p c781617 c781615))
|||
|||1. (~ (p c781615 c781617))
|||2. (~ (pp-1 c781617 c781615))
|||3. (~ (ntpp-1 c781617 c781615))
|||4. (~ (tpp-1 c781617 c781615))
|||5. (~ (po c781617 c781615))
|||6. (~ (ec c781617 c781615))
|||7. (~ (dc c781617 c781615))
|||8. (dc c781616 c781615)
|||9. (po c781617 c781616)
|||
|||> ((~ (p X Z)) <-- (po X Y) (dc Y Z))
||||=============================
||||Step 11
||||
||||? (po c781617 Var63)
||||
||||1. (p c781617 c781615)
||||2. (~ (p c781615 c781617))
||||3. (~ (pp-1 c781617 c781615))
||||4. (~ (ntpp-1 c781617 c781615))
||||5. (~ (tpp-1 c781617 c781615))
||||6. (~ (po c781617 c781615))
||||7. (~ (ec c781617 c781615))
||||8. (~ (dc c781617 c781615))
||||9. (dc c781616 c781615)
||||10. (po c781617 c781616)
||||
||||> hyp
|||=============================
|||Step 12
|||
|||? (dc c781616 c781615)
|||
|||1. (p c781617 c781615)
|||2. (~ (p c781615 c781617))
|||3. (~ (pp-1 c781617 c781615))
|||4. (~ (ntpp-1 c781617 c781615))
|||5. (~ (tpp-1 c781617 c781615))
|||6. (~ (po c781617 c781615))
|||7. (~ (ec c781617 c781615))
|||8. (~ (dc c781617 c781615))
|||9. (dc c781616 c781615)
|||10. (po c781617 c781616)
|||
|||> hyp
||=============================
||Step 13
||
||? (~ (po c781617 c781615))
||
||1. (~ (p c781615 c781617))
||2. (~ (pp-1 c781617 c781615))
||3. (~ (ntpp-1 c781617 c781615))
||4. (~ (tpp-1 c781617 c781615))
||5. (~ (po c781617 c781615))
||6. (~ (ec c781617 c781615))
||7. (~ (dc c781617 c781615))
||8. (dc c781616 c781615)
||9. (po c781617 c781616)
||
||> hyp
|=============================
|Step 14
|
|? (~ (p c781617 c781615))
|
|1. (~ (pp-1 c781617 c781615))
|2. (~ (ntpp-1 c781617 c781615))
|3. (~ (tpp-1 c781617 c781615))
|4. (~ (po c781617 c781615))
|5. (~ (ec c781617 c781615))
|6. (~ (dc c781617 c781615))
|7. (dc c781616 c781615)
|8. (po c781617 c781616)
|
|> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
||=============================
||Step 15
||
||? (c Var69 c781617)
||
||1. (p c781617 c781615)
||2. (~ (pp-1 c781617 c781615))
||3. (~ (ntpp-1 c781617 c781615))
||4. (~ (tpp-1 c781617 c781615))
||5. (~ (po c781617 c781615))
||6. (~ (ec c781617 c781615))
||7. (~ (dc c781617 c781615))
||8. (dc c781616 c781615)
||9. (po c781617 c781616)
||
||> ((c Y X) <-- (c X Y))
||=============================
||Step 16
||
||? (c c781617 Var69)
||
||1. (~ (c Var69 c781617))
||2. (p c781617 c781615)
||3. (~ (pp-1 c781617 c781615))
||4. (~ (ntpp-1 c781617 c781615))
||5. (~ (tpp-1 c781617 c781615))
||6. (~ (po c781617 c781615))
||7. (~ (ec c781617 c781615))
||8. (~ (dc c781617 c781615))
||9. (dc c781616 c781615)
||10. (po c781617 c781616)
||
||> ((c X Y) <-- (o X Y))
||=============================
||Step 17
||
||? (o c781617 Var69)
||
||1. (~ (c c781617 Var69))
||2. (~ (c Var69 c781617))
||3. (p c781617 c781615)
||4. (~ (pp-1 c781617 c781615))
||5. (~ (ntpp-1 c781617 c781615))
||6. (~ (tpp-1 c781617 c781615))
||7. (~ (po c781617 c781615))
||8. (~ (ec c781617 c781615))
||9. (~ (dc c781617 c781615))
||10. (dc c781616 c781615)
||11. (po c781617 c781616)
||
||> ((o X Y) <-- (po X Y))
||=============================
||Step 18
||
||? (po c781617 Var69)
||
||1. (~ (o c781617 Var69))
||2. (~ (c c781617 Var69))
||3. (~ (c Var69 c781617))
||4. (p c781617 c781615)
||5. (~ (pp-1 c781617 c781615))
||6. (~ (ntpp-1 c781617 c781615))
||7. (~ (tpp-1 c781617 c781615))
||8. (~ (po c781617 c781615))
||9. (~ (ec c781617 c781615))
||10. (~ (dc c781617 c781615))
||11. (dc c781616 c781615)
||12. (po c781617 c781616)
||
||> hyp
|=============================
|Step 19
|
|? (~ (c c781616 c781615))
|
|1. (p c781617 c781615)
|2. (~ (pp-1 c781617 c781615))
|3. (~ (ntpp-1 c781617 c781615))
|4. (~ (tpp-1 c781617 c781615))
|5. (~ (po c781617 c781615))
|6. (~ (ec c781617 c781615))
|7. (~ (dc c781617 c781615))
|8. (dc c781616 c781615)
|9. (po c781617 c781616)
|
|> ((~ (c X Y)) <-- (dc X Y))
|=============================
|Step 20
|
|? (dc c781616 c781615)
|
|1. (c c781616 c781615)
|2. (p c781617 c781615)
|3. (~ (pp-1 c781617 c781615))
|4. (~ (ntpp-1 c781617 c781615))
|5. (~ (tpp-1 c781617 c781615))
|6. (~ (po c781617 c781615))
|7. (~ (ec c781617 c781615))
|8. (~ (dc c781617 c781615))
|9. (dc c781616 c781615)
|10. (po c781617 c781616)
|
|> hyp
=============================
Step 21

? (~ (tpp-1 c781617 c781615))

1. (~ (ntpp-1 c781617 c781615))
2. (~ (tpp-1 c781617 c781615))
3. (~ (po c781617 c781615))
4. (~ (ec c781617 c781615))
5. (~ (dc c781617 c781615))
6. (dc c781616 c781615)
7. (po c781617 c781616)

> hyp
